COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00009 00003	.skip 1
C00010 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.require "mtcpub.pub[let,jmc]" source;
.cb GOEDEL'S LEMMA AND APPLICATIONS IN FIRST ORDER LISP

	The object of this note is to give a compact treatment of Goedel's
Lemma in an axiomatization of Lisp in a first order logic fortified by
first order lambda notation.  The Lisp Goedel numbering trivial by
letting expressions be their own Goedel numbers, and the first order
lambdas enable one to avoid the circumlocutions of the conventional
treatment.  The circumlocutions arise from the fact that Goedel's lemma is
really about the application of first order predicate expressions to
themselves, but a logic not admitting complex predicate expressions has to
get around this fact by using wffs with one free variable and taking this
variable to be ⊗x or some other standard name.

	Adding first order lambdas to first order logic does not change
its basic character, because any wff containing them can be transformed
to an equivalent wff without them by making the indicated lambda
conversions.  As will be seen, however, it makes the metamathematics
simpler, and it has other advantages for mathematical theory of
computation.

	Goedel's lemma is a key technical result making possible proofs of
Goedel's incompleteness theorems in various forms, Tarski's theorem on the
undefinability of truth, and other negative results of recursive function
theory and formalized arithmetic.  Goedel imbedded a special case in a
longer proof, and other authors have isolated it.  For an elegant
conventional treatment we refer to (Boolos and Jeffrey 1974).

	Let ⊗p be a one argument predicate expression in Lisp.  We
define

!!a1:	%2diag p ← <p <" p>>%1,

which becomes

!!a1a:	%2(∀p)(diag(p) = <p <" p>>)%1

as a formula of logic and

!!a2:	%1(DEF (DIAG P) (L P (L (" ") P))))%1

in compact S-expression Lisp.  As a formula in a first order axiomatization
of Lisp written in S-expressions, it would be

!!a2a:	%1(∀ (P) (= (DIAG P) (L P (L (" ") P))))%1.

	Let ⊗b be a one place predicate expression, and consider the
sentence

!!a3:	%2g = ((λ (P) (b (DIAG P))) (" (λ (P) (b (DIAG P)))))%1.

Performing the lambda conversion indicated in ({eq a3})
and carrying out the indicated evaluations of DIAG applied to
quoted arguments gives

.BEGIN NOFILL

!!a4:	%2g ∂(15)= ((λ (P) (b (DIAG P))) (" (λ (P) (b (DIAG P)))))%1.

∂(15)= (b (DIAG (" (λ (P) (b (DIAG P))))))%1

∂(15)= (b (L (" (λ (P) (b (DIAG P)))) (L (" ") (" (λ (P) (b (DIAG P)))) )))%1

∂(15)= (b (L (" (λ (P) (b (DIAG P)))) (" (" (λ (P) (b (DIAG P))))) ))%1

∂(15)= (b (" ((λ (P) (b (DIAG P))) (" (λ (P) (b (DIAG P))))) ))%1

∂(15)= (b (" g))%1

.end
.if false then begin
(" (λ (P) (b (DIAG P))))
.end

	Goedel's Lemma then takes the form

%2Theorem - If b is a predicate expression of one argument in our
first order language of Lisp, then there is a wff g satisfying

!!a5:	%8r%2 g ≡ b <" g>

or in S-expression form

!!a6:	%1(THEOREM (≡ g (b (LIST (" ") g)))).

	The proof is just the above calculation.  The only rules
used are lambda conversion, which is part of the logic with first
order lambdas, and the computation of the Lisp function LIST applied
to constant arguments.

Remark: In the above form, Goedel's lemma is just an imitation
of a fixed point theorem of the lambda calculus, i.e. that
[λ x f(x(x))][λ x f(x(x))] converts to 
f([λ x f(x(x))][λ x f(x(x))]) and is therefore a fixed point
of f.  It is proved by just carrying out the indicated lambda conversion.

Notational confession: A desire for compactness has led to
compressing Lisp notation according to the following table:

	" for QUOTE
	λ for LAMBDA
	L for LIST.

Further confession: The afore-used S-expression theory of Lisp
hasn't been written down.  It is along the lines of (Cartwright
and McCarthy 1979) but in S-expressions and simpler.  Since
only a version analogous to Abraham Robinson's Q is required,
we don't need induction but only the algebraic properties
of the basic functions and the recursive formula

!!a7:	%2x ≤ y ≡ atom x ∨ [¬atom y ∧ [x = y ∨ x ≤ qa y ∨ x ≤ qd y]]%1.

Maybe Goedel's lemma doesn't even require ≤.

	The applications promised in the title are yet to come.
.skip 2
References:

%3Boolos, George and Richard Jeffrey (1974)%1: %2Computability and Logic%1,
Cambridge University Press.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This version of
GOEDEL[W79,JMC]
translated for printing (by PUB) at {time} on {date}.%1